File descent.ML

(*  Title:       HOL/Tools/function_package/descent.ML
    Author:      Alexander Krauss, TU Muenchen

Descent proofs for termination
*)


signature DESCENT =
sig

  val derive_diag : Proof.context -> tactic -> (Termination.data -> int -> tactic)
                    -> Termination.data -> int -> tactic

  val derive_all  : Proof.context -> tactic -> (Termination.data -> int -> tactic)
                    -> Termination.data -> int -> tactic

end


structure Descent : DESCENT =
struct

fun gen_descent diag ctxt tac cont D = Termination.CALLS (fn (cs, i) =>
  let
    val thy = ProofContext.theory_of ctxt
    val measures_of = Termination.get_measures D

    fun derive c D =
      let
        val (_, p, _, q, _, _) = Termination.dest_call D c
      in
        if diag andalso p = q
        then fold (fn m => Termination.derive_descent thy tac c m m) (measures_of p) D
        else fold_product (Termination.derive_descent thy tac c)
               (measures_of p) (measures_of q) D
      end
  in
    cont (FundefCommon.PROFILE "deriving descents" (fold derive cs) D) i
  end)

val derive_diag = gen_descent true
val derive_all = gen_descent false

end