Defarbrec-event-generation
Event generation performed by defarbrec.
Some events are generated in two slightly different forms:
a form that is local to the generated encapsulate,
and a form that is exported from the encapsulate.
Proof hints are in the former but not in the latter,
thus keeping the ACL2 history ``clean''.
Other events are generated only locally in the encapsulate,
without any exported counterparts.
These have automatically generated fresh names:
the names used so far
are threaded through the event generation functions below.
Other events are only exported from the encapsulate,
without any local counterparts.
The generated events, and particularly the proofs hints,
follow the template in the file defarbrec-template.lisp,
which is referred to as `template'
in the documentation of the event generation functions below.
Subtopics
- Defarbrec-gen-everything
- Generate the top-level event.
- Defarbrec-gen-fn-fn
- Generate the definition of the lfn function.
- Defarbrec-gen-measure-fn-end-lemma
- Generate the local lemma about the generated measure function
that asserts that
iterating the argument updates on terminating arguments
for the number indicated by the generated measure function
yields values satisfying the exit test.
- Defarbrec-gen-measure-fn-min-lemma
- Generate the local lemma about the generated measure function
that asserts that the value of the measure function is
the minimum number of iterations of the argument update functions
that turn terminating arguments into values satisfying the exit test.
- Defarbrec-gen-measure-fn
- Generate the measure function definition.
- Defarbrec-gen-update-fns
- Generate the iterated argument update function definitions.
- Defarbrec-gen-terminates-fn
- Generate the termination testing predicate definition.
- Defarbrec-gen-measure-fn-natp-lemma
- Generate the local lemma about the generated measure function
that asserts that the measure function returns a natural number.
- Defarbrec-gen-update-fns-lemma
- Generate the local lemma
about the iterated argument udpate functions.
- Defarbrec-gen-extend-table
- Generate the event that extends the defarbrec table.
- Defarbrec-gen-test-of-updates-term
- Generate the instantiation of the exit test of fn
with calls to the iterated argument update functions.
- Defarbrec-gen-var-k
- Generate the variable k that counts
the iterated updates of the arguments.
- Defarbrec-gen-var-l
- Generate the variable l that counts
the iterated updates of the arguments.
- Defarbrec-gen-print-result
- Generate the events that print the results.
