----------------------------------------------------------------------
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

SYNOPSIS
The general depth consequence conversion of which
{DEPTH_CONSEQ_CONV}, {REDEPTH_CONSEQ_CONV}, {ONCE_DEPTH_CONSEQ_CONV} etc
are just instantiations.

DESCRIBE
{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.

SEEALSO
ConseqConv.DEPTH_CONSEQ_CONV, ConseqConv.REDEPTH_CONSEQ_CONV,
ConseqConv.ONCE_DEPTH_CONSEQ_CONV, ConseqConv.NUM_DEPTH_CONSEQ_CONV.

----------------------------------------------------------------------