EXT_DEPTH_CONSEQ_CONV congruence_list cache_opt step_opt redepth convL is the conversion used by these other depth conversions. Its interface allows one to add to the given list of boolean combinations and thus allow the conversion of parts of user-defined predicates. This is done using congruence_list. However, let’s consider the other parameters first: 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.

The first parameter congruence_list is a list of congruences 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 gives the context that can be used, but is normally just interesting for the conversions. If you ignore the number of steps, 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. As an example, a congruence for implications is implemented by

fun CONSEQ_CONV_CONGRUENCE___imp_simple_context context sys dir t =
  let
     val (b1,b2) = dest_imp t;

     (* simplify the precondition *)
     val (n1, thm1_opt) = sys [] 0 (CONSEQ_CONV_DIRECTION_NEGATE dir) b1;

     (* what did it simplify to? *)
     val a2 = CONSEQ_CONV___OPT_GET_SIMPLIFIED_TERM
                thm1_opt
                (CONSEQ_CONV_DIRECTION_NEGATE dir)
                b1;

     (* if precond is false, one does not need to process the conclusion *)
     val abort_cond = same_const a2 F;

     (* otherwise process the conclusion and add the precond as
        additional context *)
     val (n2, thm2_opt) = if abort_cond then (n1, NONE)
                          else sys [a2] n1 dir b2;

     (* abort, if nothing was done *)
     val _ = if (isSome thm1_opt) orelse (isSome thm2_opt) orelse
                abort_cond
             then ()
             else raise UNCHANGED;

     (* get theorems, if necessary create them and get the additional
        context as an additional implication *)
     val thm1 = conseq_conv_congruence_EXPAND_THM_OPT (thm1_opt, b1, NONE);
     val thm2 = conseq_conv_congruence_EXPAND_THM_OPT (thm2_opt, b2, SOME a2);

     (* apply congruence rule for these theorems *)
     val cong_thm =
         if (dir = CONSEQ_CONV_STRENGTHEN_direction) then
           IMP_CONG_simple_imp_strengthen
         else IMP_CONG_simple_imp_weaken
     val thm3 = MATCH_MP cong_thm (CONJ thm1 thm2)

     (* simplify output: (F ==> X) = X etc.
     val thm4 = CONV_RULE (dir_conv dir trivial_imp_simp) thm3
                 handle HOL_ERR _ => thm3
  in
     (n2, thm4)
  end handle HOL_ERR _ => raise CONSEQ_CONV_congruence_expection;