DEPTH_CONSEQ_CONV
ConseqConv.DEPTH_CONSEQ_CONV : directed_conseq_conv -> directed_conseq_conv
Applies a consequence conversion repeatedly to all the sub-terms of a term, in top-down order.
DEPTH_CONSEQ_CONV c tm tries to apply the given conversion at
toplevel. If this fails, it breaks the term tm down into boolean
subterms. It can break up the following operators: /\, \/, ~,
==> and quantification. Then it applies the directed consequence
conversion c to terms and iterates. Finally, it puts everything
together again.
Notice that some operators switch the direction that is passed to c,
e.g. to strengthen a term ~t, DEPTH_CONSEQ_CONV tries to weaken t.
Example
Consider the expression FEVERY P (f |+ (x1, y1) |+ (x2,y2)). It states
that all elements of the finite map f |+ (x1, y1) |+ (x2, y2) satisfy
the predicate P. However, the definition of x1 and x2 possible
hide definitions of these keys inside f or in case x1 = x2 the
middle update is void. You easily get into a lot of aliasing problems
while proving thus a statement. However, the following theorem holds:
|- !f x y. FEVERY P (f |+ (x,y)) /\ P (x,y) ==> FEVERY P (f |+ (x,y))
Given a directed consequence conversion c that instantiates this
theorem, DEPTH_CONSEQ_CONV can be used to apply it repeatedly and at
substructures as well:
DEPTH_CONSEQ_CONV c CONSEQ_CONV_STRENGTHEN_direction
``!y2. FEVERY P (f |+ (x1, y1) |+ (x2,y2)) /\ Q z`` =
|- (!y2. FEVERY P f /\ P (x1, y1) /\ P (x2,y2) /\ Q z) ==>
(!y2. FEVERY P (f |+ (x1, y1) |+ (x2,y2)) /\ Q z)
See also
Conv.DEPTH_CONV,
ConseqConv.ONCE_DEPTH_CONSEQ_CONV,
ConseqConv.NUM_DEPTH_CONSEQ_CONV,
ConseqConv.DEPTH_STRENGTHEN_CONSEQ_CONV,
ConseqConv.REDEPTH_CONSEQ_CONV