EXT_DEPTH_CONSEQ_CONV
ConseqConv.EXT_DEPTH_CONSEQ_CONV : conseq_conv_congruence list ->
depth_conseq_conv_cache_opt -> int option ->
bool ->
(bool * int option * (thm list -> directed_conseq_conv)) list ->
thm list ->
directed_conseq_conv
The general depth consequence conversion of which DEPTH_CONSEQ_CONV,
REDEPTH_CONSEQ_CONV, ONCE_DEPTH_CONSEQ_CONV etc are just
instantiations.
DEPTH_CONSEQ_CONV and similar conversions are able to apply a
consequence conversion by breaking down the structure of a term using
lemmata about /\, \/, ~, ==>, if-then-else and quantification.
While doing so, these conversions collect various amounts of context
information. EXT_DEPTH_CONSEQ_CONV congruence_list cache_opt
step_opt redepth convL context is the function used by these
other depth conversions. For this purpose, the
cache_opt determines which cache to use: NONE means no caching; a
standard cache that stores everything is configured by
CONSEQ_CONV_default_cache_opt.
The number of steps taken is determined by step_opt. NONE means
arbitrarily many; SOME n means at most n. ONCE_DEPTH_CONSEQ_CONV for
example uses SOME 1. The parameter redepth determines whether
modified terms should be revisited and convL is a basically a list of
directed consequence conversions of the conversions that should be
applied at subpositions. Its entries consist of a flag, whether to apply
the conversion before or after descending into subterms; the weight
(i.e. the number of counted steps) for the conversion, and a function
from the context (a list of theorems) to the conversion. context
provides additional context that might be used.
The first parameter congruence_list is a list of congruence functions
that determine how to break down terms. Each element of this list has to
be a function congruence context sys dir t which returns a pair of the
number of performed steps and a resulting theorem. sys is a callback
that allows to apply the depth conversion recursively to subterms.
context represents the context that can be used. If you ignore the
slightly different return type, the congruence is otherwise a directed
consequence conversion. If the congruence can't be applied, it should
either fail or raise an UNCHANGED exception. The callback sys gets
the number of already performed steps, a direction and a term. It then
returns a accumulated number of steps and a thm option. It never fails.
The number of steps is used to abort if the maximum number of globally
allowed steps has been reached. The first call of sys should get 0,
then the accumulated number has to be passed. The congruence should
return the finally accumulated number of steps.
See also
ConseqConv.DEPTH_CONSEQ_CONV,
ConseqConv.REDEPTH_CONSEQ_CONV,
ConseqConv.ONCE_DEPTH_CONSEQ_CONV,
ConseqConv.NUM_DEPTH_CONSEQ_CONV